Problem:
 a__f(0()) -> cons(0(),f(s(0())))
 a__f(s(0())) -> a__f(a__p(s(0())))
 a__p(s(0())) -> 0()
 mark(f(X)) -> a__f(mark(X))
 mark(p(X)) -> a__p(mark(X))
 mark(0()) -> 0()
 mark(cons(X1,X2)) -> cons(mark(X1),X2)
 mark(s(X)) -> s(mark(X))
 a__f(X) -> f(X)
 a__p(X) -> p(X)

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {8,7,6}
   transitions:
    f3(27) -> 28*
    f3(24) -> 18,8
    p1(5) -> 7*
    p1(2) -> 7*
    p1(4) -> 7*
    p1(1) -> 7*
    p1(3) -> 7*
    03() -> 24*
    f1(10) -> 11*
    f1(5) -> 6*
    f1(2) -> 6*
    f1(4) -> 6*
    f1(1) -> 6*
    f1(3) -> 6*
    cons3(24,28) -> 18,8
    s1(9) -> 10*
    s1(18) -> 18,8
    s3(24) -> 27*
    mark1(5) -> 18*
    mark1(2) -> 18*
    mark1(4) -> 18*
    mark1(1) -> 18*
    mark1(3) -> 18*
    cons1(18,1) -> 18,8
    cons1(18,3) -> 18,8
    cons1(18,5) -> 18,8
    cons1(18,2) -> 18,8
    cons1(18,4) -> 18,8
    cons1(9,11) -> 6*
    01() -> 18,8,7,9
    a__p1(10) -> 16*
    a__p1(18) -> 18,8
    a__f1(16) -> 6*
    a__f1(18) -> 18,8
    p2(10) -> 16*
    p2(18) -> 18,8
    a__f0(5) -> 6*
    a__f0(2) -> 6*
    a__f0(4) -> 6*
    a__f0(1) -> 6*
    a__f0(3) -> 6*
    f2(19) -> 20*
    f2(16) -> 6*
    f2(18) -> 18,8
    00() -> 1*
    02() -> 8,18,16
    cons0(3,1) -> 2*
    cons0(3,3) -> 2*
    cons0(3,5) -> 2*
    cons0(4,2) -> 2*
    cons0(4,4) -> 2*
    cons0(5,1) -> 2*
    cons0(5,3) -> 2*
    cons0(5,5) -> 2*
    cons0(1,2) -> 2*
    cons0(1,4) -> 2*
    cons0(2,1) -> 2*
    cons0(2,3) -> 2*
    cons0(2,5) -> 2*
    cons0(3,2) -> 2*
    cons0(3,4) -> 2*
    cons0(4,1) -> 2*
    cons0(4,3) -> 2*
    cons0(4,5) -> 2*
    cons0(5,2) -> 2*
    cons0(5,4) -> 2*
    cons0(1,1) -> 2*
    cons0(1,3) -> 2*
    cons0(1,5) -> 2*
    cons0(2,2) -> 2*
    cons0(2,4) -> 2*
    a__f2(24) -> 8,18
    f0(5) -> 3*
    f0(2) -> 3*
    f0(4) -> 3*
    f0(1) -> 3*
    f0(3) -> 3*
    a__p2(19) -> 24*
    s0(5) -> 4*
    s0(2) -> 4*
    s0(4) -> 4*
    s0(1) -> 4*
    s0(3) -> 4*
    s2(16) -> 19*
    a__p0(5) -> 7*
    a__p0(2) -> 7*
    a__p0(4) -> 7*
    a__p0(1) -> 7*
    a__p0(3) -> 7*
    cons2(16,20) -> 6,18,8
    mark0(5) -> 8*
    mark0(2) -> 8*
    mark0(4) -> 8*
    mark0(1) -> 8*
    mark0(3) -> 8*
    p3(19) -> 24*
    p0(5) -> 5*
    p0(2) -> 5*
    p0(4) -> 5*
    p0(1) -> 5*
    p0(3) -> 5*
  problem:
   
  Qed